00100	OP
00200	←(V1,A1)
00300	NIL
00400	NIL
00500	NIL
00600	ISVAR(V1);;
00700	C(V1,A1);;
00800	
00900	
01000	ITERATIVE
01100	TUNIFY
01200	NIL
01300	NIL
01400	NIL
01500	NEWVAR(V7);NEWVAR(V8);NEWVAR(V12);NEWVAR(V13);
01600	VUNIFY(V4,V5,V6);
01700	C(V12 V1);C(V13 V2);C(V3,V4);C(V7,V5);C(V8,V6);;
01800	C(V3,V9);C(V7,V10);C(V8,V11);C(V12,V14);C(V13,V15);
01900	VUNIFY(V9,V10,V11);;
02000	CUNIFY1(V3 V9(SUBST* V9 (CAR* V14))(SUBST* V9(CAR* V15)));
02100	C(V7, (CONS* V10, (CAR* V14)));C(V8,(CONS* V11, (CAR* V15)));
02200	C(V12, (CDR* V14));C(V13, (CDR* V15));;
02300	=(V14,NIL*);;
02400	UNIFY(V3 V1 V2);;
02500	UNIFY(V3 V1 V2);;
02600	
02700	OP
02800	VARVAR(V3,V9,T1,T2)
02900	NIL
03000	NIL
03100	NIL
03200	VAR(T1);VAR(T2);C(V3,(COMPOSE* T1 T2 V9));;
03300	CUNIFY1(V3,V9,T1,T2);;
03400	
03402	OP
03404	VAR_VARNOT(V3,V9,T1,T2)
03406	NIL
03408	NIL
03410	NIL
03412	VAR(T1);¬VAR(T2);¬OCCUR(T1,T2);C(V3,(COMPOSE* T1 T2 V9));;
03414	CUNIFY1(V3,V9,T1,T2);;
03416	
03418	
03420	OP
03422	VARNOT_VAR(V3 V9 T1 T2)
03424	NIL
03426	NIL
03428	NIL
03430	VAR(T2);¬VAR(T1);¬OCCUR(T2,T1); C(V3,(COMPOSE* T2 T1 V9));;
03432	CUNIFY1(V3 V9 T1 T2);;
03434	
03436	OP
03438	VARNOT_VARNOT(V3 V9 T1 T2)
03440	NIL
03442	NIL
03444	NIL
03446	¬VAR(T1);¬VAR(T2); =((FL* T1), (FL* T2));C(V3(COMPOSEL* (TERMS* T1) (TERMS* T2)V9));;
03448	CUNIFY1(V3 V9 T1 T2);;
03450	
03500	AXIOM
03600	TAUNIFY
03700	NIL
03800	T
03900	NIL
04000	=(V10,V10);;
04100	VUNIFY(V9,V10,V11);;
04200	
04300	
04400	NIL
04500	NIL
04600	
04700	ISVAR(Z);VAR(A);VAR(B);VUNIFY(NIL* NIL* NIL*);;
04800	
04900	T
05000	
05100	((C T NIL NIL (X,*))
05200	(VAR T T NIL NIL)
05300	(= T NIL NIL NIL)
05400	(CUNIFY T NIL NIL NIL )
05500	(CUNIFY1 T NIL NIL NIL)
05600	(VUNIFY T NIL NIL NIL)
05700	(UNIFY T NIL NIL NIL))
05800	
05900	
06000	
06100	NIL
06200